$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $x$, $y$:$A$, $v$:$B$($x$), $u$:$B$($y$).
\\[0ex]($x$ $=$ $y$ $\Rightarrow$ $v$ $=$ $u$ $\in$ $B$($x$)) $\Rightarrow$ $x$ : $v$ $\parallel$ $y$ : $u$